Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    g(A)  → A
2:    g(B)  → A
3:    g(B)  → B
4:    g(C)  → A
5:    g(C)  → B
6:    g(C)  → C
7:    foldf(x,nil)  → x
8:    foldf(x,cons(y,z))  → f(foldf(x,z),y)
9:    f(t,x)  → f'(t,g(x))
10:    f'(triple(a,b,c),C)  → triple(a,b,cons(C,c))
11:    f'(triple(a,b,c),B)  → f(triple(a,b,c),A)
12:    f'(triple(a,b,c),A)  → f''(foldf(triple(cons(A,a),nil,c),b))
13:    f''(triple(a,b,c))  → foldf(triple(a,b,nil),c)
There are 8 dependency pairs:
14:    FOLDF(x,cons(y,z))  → F(foldf(x,z),y)
15:    FOLDF(x,cons(y,z))  → FOLDF(x,z)
16:    F(t,x)  → F'(t,g(x))
17:    F(t,x)  → G(x)
18:    F'(triple(a,b,c),B)  → F(triple(a,b,c),A)
19:    F'(triple(a,b,c),A)  → F''(foldf(triple(cons(A,a),nil,c),b))
20:    F'(triple(a,b,c),A)  → FOLDF(triple(cons(A,a),nil,c),b)
21:    F''(triple(a,b,c))  → FOLDF(triple(a,b,nil),c)
The approximated dependency graph contains one SCC: {14-16,18-21}.
Tyrolean Termination Tool  (10.81 seconds)   ---  May 3, 2006